(IN-PACKAGE "ACL2")

(DEFUN EQUAL2 (X Y) (AND (= X Y) T))

